DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2020.29

Semi-Axiomatic Sequent Calculus

Authors: Henry DeYoung, Frank Pfenning, and Klaas Pruiksma

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract

We present the semi-axiomatic sequent calculus (SAX) that blends features of Gentzen’s sequent calculus with an axiomatic formulation of intuitionistic logic. We develop and prove a suitable analogue to cut elimination and then show that a natural computational interpretation of SAX provides a simple form of shared memory concurrency.

Cite as

Henry DeYoung, Frank Pfenning, and Klaas Pruiksma. Semi-Axiomatic Sequent Calculus. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{deyoung_et_al:LIPIcs.FSCD.2020.29,
  author =	{DeYoung, Henry and Pfenning, Frank and Pruiksma, Klaas},
  title =	{{Semi-Axiomatic Sequent Calculus}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{29:1--29:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.29},
  URN =		{urn:nbn:de:0030-drops-123515},
  doi =		{10.4230/LIPIcs.FSCD.2020.29},
  annote =	{Keywords: Sequent calculus, Curry-Howard isomorphism, shared memory concurrency}
}

Search Results

Documents authored by Pruiksma, Klaas

Semi-Axiomatic Sequent Calculus

Abstract

Cite as

Thanks for your feedback!

Could not send message